Inference at * 1 0 
Iof proof for Lemma symmetrized preorder:



1. T : Type
2. R : TT
3. Refl(T;x,y.R(x,y))
4. Trans(T;x,y.R(x,y))
  Refl(T;a,b.R(a,b) & R(b,a)) 

latex

 by PERMUTE{1:n, 1:n, 2:n} 

latex

 1: .....wf..... NILNIL

 1: 3. a:T. R(a,a)
 1: 4. Trans(T;x,y.R(x,y))
 1: 5. a : T
 1:   a  T
 2: .....wf..... NILNIL

 2: 3. a:T. R(a,a)
 2: 4. Trans(T;x,y.R(x,y))
 2:   T  Type
 .

Definitions

t  T, f(a), s = t, x:A  B(x), Trans(T;x,y.E(x;y)), x(s1,s2), , x:AB(x), Type, x:A. B(x), P & Q, Refl(T;x,y.E(x;y))